00010	VAR:x,y,z,u,s;
00020	INF_PRED:=;PRE_PRED:clear,on;
00030	PRE_OP: puton,A,B,C,T,S0,R;
00040	
00100	clear(x)∧clear(y)⊃on(x,y);
00200	clear(x)⊃on(x,T);
00300	clear(x) ≡ ∀y¬on(y,x);
00400	on(x,y)⊃clear(y);
00500	
00800	clear(C); clear(B); 
00900	on(A,T); on(B,T); on(C,A);
00950	¬A=B; ¬B=C; ¬C=A; ¬A=T;¬B=T; ¬C=T;
00975	-A=C; A=A; ¬B=A; B=B; ¬C=B; C=C;¬T=A;¬T=B;¬T=C;T=T;
01000	THM: on(B,C)∧on(A,B);;